p:FinProbSpace. Normal(Outcome) 

latex

Definitions	Normal(T), Outcome, FinProbSpace, x:A. B(x), #$n, t  T, , ||as||, n+m, i  j , x,y:A//B(x;y), type List, s = t, r  s, xL. P(x), a < b, A  B, x:A  B(x), P & Q, i  j < k, Void, x:AB(x), P  Q, False, A, {x:A| B(x)} , {i..j}, , , A c B, [], l[i], x.A(x), , A  B, , EquivRel(T;x,y.E(x;y)), qeq(r;s), , x,y. t(x;y), Type, left + right, if b then t else f fi , x. t(x), tt, P  Q, P  Q
Lemmas	int-eq-in-rationals, sum unroll base q, b-union wf, int nzero wf, btrue wf, tunion wf, bool wf, ifthenelse wf, int-rational, quotient wf, qeq wf2, select wf, length wf2, int seg wf, le wf, non neg length, length wf1, rationals wf